Inference at * 
Iof proof for Lemma assert of eq int rw:


  x,y:. {((x = y))  (x = y)} 

latex

 by ((Unfold `guard` 0) 
CollapseTHEN (Lemma `assert_of_eq_int`)) 

latex

C.

Definitions	{T}
Lemmas	assert of eq int